|
|
Comparison of conventional CT and VT with current and voltage sensors
Dvořák, Petr ; Drápela, Jiří (referee) ; Orságová, Jaroslava (advisor)
The diploma thesis deals with conventional transformers and current and voltage sensors. The first half of thesis describes mainly the basic concepts and accuracy classes of these converters used in electrical substations. The emphasis is given primarily on the differences. In the second half of thesis is presented an exact type of converters, which are installed in the substation Medlánky. There is an analysis of measured data from long – term monitoring from this substation and comparing the results from conventional transformers compared to the results from more modern sensors.
|
|
|
Tool for Abstract Regular Model Checking
Chalk, Matěj ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.
|
|
|
Synchronous Formal Systems Based on Grammars and Transducers
Horáček, Petr ; Janoušek, Jan (referee) ; Yamamura,, Akihito (referee) ; Meduna, Alexandr (advisor)
Tato disertační práce studuje synchronní formální systémy založené na gramatikách a převodnících a zkoumá jak jejich teoretické vlastnosti, tak i perspektivy praktických aplikací. Práce představuje nové koncepty a definice vycházející ze známých principů řízeného přepisování a synchronizace. Navrhuje alternativní způsob synchronizace bezkontextových gramatik, založený na propojení pravidel. Tento princip rozšiřuje také na řízené gramatiky, konkrétně gramatiky s rozptýleným kontextem a maticové gramatiky. Dále je představen na podobném principu založený nový druh převodníku, tzv. pravidlově omezený převodník. Jedná se o systém složený z konečného automatu a bezkontextové gramatiky. Práce prezentuje nové teoretické výsledky ohledně generativní a přijímajicí síly. Poslední část práce zkoumá možnosti lingvisticky orientovaných aplikací se zameřením na překlad přirozeného jazyka. Diskutuje a srovnává hlavní výhody nových modelů s využitím vybraných případových studií z českého, anglického a japonského jazyka pro ilustraci.
|
|
|
Classifications in the construction industry, their development and use
Vydrová, Michaela ; Dvořák, Jiří (referee) ; Nový, Martin (advisor)
The theoretical part of the bachelor´s thesis discusses the importance of classification in construction. It describes the historical development and the importance of classification in the construction industry. Monitors use classifications and classifications in practice and use in the Czech legislation. The practical part deals with specific examples of classification of buildings and construction work. Part of the work is concerned with finding house prices in a period other than the planned construction.
|
|
|
Transducer Systems
Skácel, Jiří ; Kučera, Jiří (referee) ; Meduna, Alexandr (advisor)
This document defines systems of pushdown transducers. The idea of cooperating distributed grammar systems for components working on one word is adjusted for use of transducers instead of grammars. The transducers cooperate by passing output of one to input of another component. It discusses their descriptive power and equivalency between systems with arbitrary numbers of components. The main conclusion is then comparison of their descriptive power with Turing machines with regard to their translation and accepted languages.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
V této práci se zabýváme regulárním model checkingem, což je technika pro analýzu programů, jejíchž stavový prostor může být nekonečný v důsledku práce například s neomezenými frontami, parametry, dynamicky propojenými datovými strukturami, rekurzivními procedurami nebo řetězci. Cílem této práce bylo implementovat vylepšení stávajícího prototypu nástroje ASMA implementujícího regulárním model checking nad knihovnou Automata of Microsoftu. Provedli jsme analýzu zdrojového kódu nástroje ASMA a zopakovaly analýzy všech dostupných srovnávacích programů. Identifikovali jsme některá úzká místa a několik z nich jsme vyřešili. Zejména jsme integrovali knihovnu obsahující další redukční algoritmy do nástroje ASMA, vytvořili několik nových verzí operace reverzní konkatenace, která se v benchmarcích ukázala jako velmi nákladná, vylepšili rozhraní příkazového řádku ASMA a implementovali některé další optimalizace. Výpočetní čas se při analýze větších programů snížil o 90 %.
|
|
|
Data Acquisition and Control System of Hydroelectric Power Plant Using Internet Techniques
Sattouf, Mousa ; Přikryl, Hynek (referee) ; Richter, Aleš (referee) ; Skalický, Jiří (advisor)
Vodní energie se nyní stala nejlepším zdrojem elektrické energie na zemi. Vyrábí se pomocí energie poskytované pohybem nebo pádem vody. Historie dokazuje, že náklady na tuto elektrickou energii zůstávají konstantní v průběhu celého roku. Vzhledem k mnoha výhodám, většina zemí nyní využívá vodní energie jako hlavní zdroj pro výrobu elektrické energie.Nejdůležitější výhodou je, že vodní energie je zelená energie, což znamená, že žádné vzdušné nebo vodní znečišťující látky nejsou vyráběny, také žádné skleníkové plyny jako oxid uhličitý nejsou vyráběny, což činí tento zdroj energie šetrný k životnímu prostředí. A tak brání nebezpečí globálního oteplování. Použití internetové techniky k ovladání několika vodních elektráren má velmi významné výhody, jako snížení provozních nákladů a flexibilitu uspokojení změny poptávky po energii na straně spotřeby. Také velmi efektivně čelí velkým narušením elektrické sítě, jako je například přidání nebo odebrání velké zátěže, a poruch. Na druhou stranu, systém získávání dat poskytuje velmi užitečné informace pro typické i vědecké analýzy, jako jsou ekonomické náklady, predikce poruchy systémů, predikce poptávky, plány údržby, systémů pro podporu rozhodování a mnoho dalších výhod. Tato práce popisuje všeobecný model, který může být použit k simulaci pro sběr dat a kontrolní systémy pro vodní elektrárny v prostředí Matlab / Simulink a TrueTime Simulink knihovnu. Uvažovaná elektrárna sestává z vodní turbíny připojené k synchronnímu generátoru s budicí soustavou, generátor je připojen k veřejné elektrické síti. Simulací vodní turbíny a synchronního generátoru lze provést pomocí různých simulačních nástrojů. V této práci je upřednostňován SIMULINK / MATLAB před jinými nástroji k modelování dynamik vodní turbíny a synchronního stroje. Program s prostředím MATLAB SIMULINK využívá k řešení schematický model vodní elektrárny sestavený ze základních funkčních bloků. Tento přístup je pedagogicky lepší než komplikované kódy jiných softwarových programů. Knihovna programu Simulink obsahuje funkční bloky, které mohou být spojovány, upravovány a modelovány. K vytvoření a simulování internetových a Real Time systémů je možné použít bud‘ knihovnu simulinku Real-Time nebo TRUETIME, v práci byla použita knihovna TRUETIME.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
V této práci se zabýváme regulárním model checkingem, což je technika pro analýzu programů, jejíchž stavový prostor může být nekonečný v důsledku práce například s neomezenými frontami, parametry, dynamicky propojenými datovými strukturami, rekurzivními procedurami nebo řetězci. Cílem této práce bylo implementovat vylepšení stávajícího prototypu nástroje ASMA implementujícího regulárním model checking nad knihovnou Automata of Microsoftu. Provedli jsme analýzu zdrojového kódu nástroje ASMA a zopakovaly analýzy všech dostupných srovnávacích programů. Identifikovali jsme některá úzká místa a několik z nich jsme vyřešili. Zejména jsme integrovali knihovnu obsahující další redukční algoritmy do nástroje ASMA, vytvořili několik nových verzí operace reverzní konkatenace, která se v benchmarcích ukázala jako velmi nákladná, vylepšili rozhraní příkazového řádku ASMA a implementovali některé další optimalizace. Výpočetní čas se při analýze větších programů snížil o 90 %.
|
|
|
Comparison of conventional CT and VT with current and voltage sensors
Dvořák, Petr ; Drápela, Jiří (referee) ; Orságová, Jaroslava (advisor)
The diploma thesis deals with conventional transformers and current and voltage sensors. The first half of thesis describes mainly the basic concepts and accuracy classes of these converters used in electrical substations. The emphasis is given primarily on the differences. In the second half of thesis is presented an exact type of converters, which are installed in the substation Medlánky. There is an analysis of measured data from long – term monitoring from this substation and comparing the results from conventional transformers compared to the results from more modern sensors.
|
|
|
Tool for Abstract Regular Model Checking
Chalk, Matěj ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.
|
guest ::
